[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Specification mtd-base
enrich
   pebs, 
   eraseblock
, 
   align
, 
   error-class

with
   

   
   
   
   predicates  mtd-cons : pebs;
               mtd-valid-peb : peb;
   
   variables  m0 : nat;
              m1 : nat;
              m2 : nat;
   
   

   

   axioms mtd-cons :  ⊦ mtd-cons(pebs) ↔ (∀ n. n < # pebs → mtd-valid-peb(pebs[n]));
          used for: ls;
          mtd-valid-peb
          : ⊦   mtd-valid-peb(peb)
              ↔   # peb.data = PEB_SIZE
                ∧ (  ¬ peb.bad
                   → peb.fill ≤ PEB_SIZE ∧ is-aligned(peb.fill, EB_PAGE_SIZE) ∧ range=(peb.data, peb.fill, emptypeb, peb.fill, PEB_SIZE - peb.fill));
          used for: s, ls;

   

   
end enrich